IEEE Floats

SMTLIB2 standard IEEE Floating Point Numbers

Floating point operations are defined modulo rounding modes. Many algebraic properties of bit-vectors, integers and reals don't carry over to floating points. For example, addition is not associative.